Nuprl Definition : branch 11,40

if p:P then A(p) else B fi  == case d of inl(p) => A(p) | inr(x) => B 
latex



clarification:

branch(P;d;p.A(p);B) == case d of inl(p) => A(p) | inr(x) => B 
latex


Definitionscase b of inl(x) => s(x) | inr(y) => t(y)
FDL editor aliasesbranch

origin